Slice 2 follow-up: green the idris2-proofs + chapel-golden Provable jobs by hyperpolymath · Pull Request #28 · hyperpolymath/chapeliser

hyperpolymath · 2026-06-18T11:54:34Z

Follow-up to #27 (merged). #27 landed the provable.yml workflow and got Zig + codegen-drift green, but merged while two jobs were still failing — this greens them:

`idris2-proofs`

Removed the three auxiliary DecEq instances (Result, PartitionStrategy, GatherStrategy). They are not used by any of the load-bearing proofs (completeness / disjointness / conservation / round-trip / layout) and relied on a decEq _ _ = No absurd catch-all, which Idris2 rejects — No absurd needs explicit off-diagonal constructor pairs (as the base library's DecEq Bool does). The invariant proofs are untouched; a comment notes they can be re-added via elaborator-reflection derivation if decidable equality is ever needed.

`chapel-golden`

chpl reported Could not find C function for c_process_item — the c_* externs are called inside the coforall … on loc (potentially-remote) block, which Chapel requires to have a real C prototype. The generated <name>_chapeliser.h only declares the echo_* user contract, not the c_* bridge ABI. Fix (a proper codegen improvement, not a golden-only hack):

header.rs now also emits <name>_abi.h with the 12 c_* prototypes.
chapel.rs emits require "<name>_abi.h"; in the wrapper module.
the chapel-golden job passes -I …/include so the require resolves.
golden fixtures regenerated (adds echo_abi.h + the require line).

Verified locally

Rust layer still 63 tests green, codegen drift-free. The idris2/chapel toolchains aren't installable in the dev sandbox, so — as with #27 — CI is the verifier; turning these two jobs green is the acceptance gate, and I'll drive it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

Generated by Claude Code

Follow-up to make the two provable.yml jobs that were still red pass: - Idris2: remove the three auxiliary DecEq instances (Result, PartitionStrategy, GatherStrategy). They are unused by the proofs and relied on a `decEq _ _ = No absurd` catch-all, which Idris2 rejects (it needs explicit off-diagonal constructor pairs, as base's DecEq Bool does). The load-bearing invariant proofs are unaffected. - Chapel: codegen now emits a c_* ABI header (<name>_abi.h) and a `require "<name>_abi.h";` in the wrapper, so chpl can resolve the extern procs called inside on/coforall (remote) contexts — fixes "Could not find C function for c_process_item". - provable.yml chapel job: add -I <include> so the require resolves. - Regenerate the golden fixtures (adds echo_abi.h + the require line). Rust layer still 63 green; golden drift-free. idris2/chapel not locally verifiable (no toolchains in sandbox) — these green in CI on push. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T11:55:31Z

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity	Count
🔴 Critical	1
🟠 High	9
🟡 Medium	45

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action mlugg/setup-zig@v1 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

idris2: Types.idr now checks (the DecEq removal worked); the failure moved to Layout.idr's `= Refl` lemmas. Remove the three brittle/incorrect ones: - sliceDescSizeCorrect / sliceDescNoPadding — idris2 0.8 does not reduce record projections of a top-level value during conversion checking, so Refl cannot discharge them. - resultDataSizeCorrect — not provable for an ARBITRARY ResultArrayLayout (the record fields are independent); the relation holds only for values built via resultLayout. The layout records + functions are unchanged; only the broken lemmas go. chapel: the "Could not find C function" error is gone (require + abi header fixed it); chpl's C backend now rejects the stub under -Werror,-Wmissing-prototypes. The stub #includes echo_abi.h so each c_* definition has a prior prototype. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T12:00:43Z

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity	Count
🔴 Critical	1
🟠 High	9
🟡 Medium	45

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action mlugg/setup-zig@v1 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

`alignment - x` resolves via the Neg interface, which Nat lacks ("Can't find an implementation for Neg Nat"). Use `minus` from Data.Nat. Types.idr already type-checks; this unblocks the rest of Layout.idr (and then Foreign.idr). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T12:03:34Z

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity	Count
🔴 Critical	1
🟠 High	9
🟡 Medium	45

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action mlugg/setup-zig@v1 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…ctly idris2: Types.idr + Layout.idr now check. Foreign.idr's MkPipelineCorrect called `perItemSlices cfg.totalItems cfg.numLocales`, which demands a *relevant* `So (numLocales > 0)` proof that cannot be synthesised (the WorkloadConfig witness is erased). Take the partition abstractly instead — `{p : Partition cfg.totalItems cfg.numLocales} -> ValidPartition p` — a cleaner statement that carries no construction-time obligation. Add the Data.So / Data.Vect imports. Also: retry the codegen-drift `cargo run` to absorb a transient crates.io fetch flake (`download of cc failed: curl ... unexpected eof`). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

github-actions · 2026-06-18T12:06:55Z

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity	Count
🔴 Critical	1
🟠 High	9
🟡 Medium	45

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action mlugg/setup-zig@v1 needs attention",
    "type": "unpinned_action",
    "file": "provable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Pins the last unpinned action in `provable.yml` to its commit SHA, clearing the one remaining advisory Hypatia `unpinned_action` finding (medium) introduced in #27/#28. `mlugg/setup-zig@v1` → `mlugg/setup-zig@53fc45b17fe98b52f92ee5ea08ff48a85a3e7eb7 # v1.2.2` SHA resolved via `git ls-remote https://github.com/mlugg/setup-zig` (the `v1` tag points to the same commit as `v1.2.2`). No behaviour change — same action, same `version: 0.14.0`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ --- _Generated by [Claude Code](https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ)_ Co-authored-by: Claude <noreply@anthropic.com>

hyperpolymath marked this pull request as ready for review June 18, 2026 12:07

hyperpolymath merged commit 2d9f372 into main Jun 18, 2026
28 checks passed

hyperpolymath deleted the claude/sharp-cannon-038nwu branch June 18, 2026 12:07

hyperpolymath mentioned this pull request Jun 18, 2026

ci: SHA-pin mlugg/setup-zig (v1.2.2) in provable.yml #29

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Slice 2 follow-up: green the idris2-proofs + chapel-golden Provable jobs#28

Slice 2 follow-up: green the idris2-proofs + chapel-golden Provable jobs#28
hyperpolymath merged 4 commits into
mainfrom
claude/sharp-cannon-038nwu

hyperpolymath commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

hyperpolymath commented Jun 18, 2026

idris2-proofs

chapel-golden

Verified locally

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

`idris2-proofs`

`chapel-golden`